w:World.
FairFifo
 (e:E. d(e;e) = 0)
 & (e, e':E. d(e;e') = d(e';e)  )
 & (e, e', e'':E. e <c e'  e' <c e''  d(e;e'') = d(e;e')+d(e';e'')) 

latex

Definitions	, t  T, {x:A| B(x) }, x:AB(x), x:A. B(x), time(e), n-m, n+m, P  Q, <a,b>, #$n, Type, Prop, True, i<j, b, b, , s = t, a<b, AB, ij, T, P  Q, x:AB(x), P & Q, P  Q, Unit, left+right, d(e;e'), World, FairFifo, E, e <c e',
Lemmas	w-causl wf, w-E wf, fair-fifo wf, world wf, eqtt to assert, assert of le int, iff transitivity, eqff to assert, squash wf, true wf, bnot of le int, assert of lt int, le int wf, le wf, bool wf, bnot wf, assert wf, lt int wf, w-causl-time, w-time wf, nat wf